the_es:event_system{i:l}, l:IdLnk. es-Msgl(the_es; l)  Type 

latex

Definitions	x:A. B(x), t  T, es-Msgl(es; l), es-Msg(es), es-M(es), t.1, t.2, event_system{i:l}, prop{i:l}
Lemmas	Msg wf, haslink wf, IdLnk wf, event system wf